ds:fpf(Id; x.Type), da:fpf(Knd; k.Type), l:( List), v:ecl-trans-tuple{i:l}(ds; da),
L:(event-info(ds;da) List), n:.
(ecl-trans-halt2(ds; da; ecl-add-catch(v; l))(n,L))
 ((((n  l))  (ecl-trans-halt2(ds; da; v)(n,L)))
  ((n = 0  )  l_exists(l; ; m.(ecl-trans-halt2(ds; da; v)(m,L))))) 

latex

Definitions

b, spreadn(u; a,b,c,d,e,f,g.v(a;b;c;d;e;f;g)), ecl-trans-h(v), ecl-trans-type(A), ecl-trans-state-from(v; z; L), ecl-trans-init(v), ecl-trans-tuple{i:l}(ds; da), t  T, x:A. B(x), P  Q, Id, x. t(x), fpf(A; a.B(a)), Knd, , event-info(ds;da), ecl-trans-halt2(ds; da; A), ecl-trans-state(v; L), ecl-add-catch(A; l), l_exists(L; T; x.P(x)), prop{i:l}, P  Q, (x  l), A, P  Q, P  Q, P  Q, ff, , bor(p; q), reduce(f; k; as), (i = j), band(p; q), nat-deq, deq-member(eq; x; L), b

Lemmas

assert of bor, assert of bnot, not functionality wrt iff, assert-deq-member, iff transitivity, assert of band, assert of eq int, bnot wf, deq-member wf, nat-deq wf, band wf, eq int wf, iff functionality wrt iff, or functionality wrt iff, and functionality wrt iff, l exists reduce, reduce wf, bor wf, bool wf, bfalse wf, not wf, l member wf, l exists wf, assert wf, event-info wf, ecl-trans-tuple wf, nat wf, Knd wf, fpf wf, Id wf, ecl-trans-state wf, ecl-trans-type wf